enrich
encoding-elem-size
,
encoding
with
axioms encoding-requires-space : ⊦ ENCODED_ELEM_SIZE ≠ 0;
used for: s, ls;
encoding-size : ⊦ encoding-size(a) = ENCODED_ELEM_SIZE;
used for: s, ls;
end enrich